step(r,(r,s),tm(s,[pri(naught,[]),pri(naught,[])],pri(lst,[pri(pc,[ctxm(beta_2_r_,dot,s,i_s,c_s),pri(enc,[pri(pc,[ctxm(beta_2_r_,dot,s,i_s,c_s),pri(enc,[ctxm(beta_2_r_,u,bsn,i_bsn,i_bsn),ctxm(beta_2_r_,dot,s_umc, (i,s_umc), (c,s_umc))]),ctxm(beta_2_r_,ci,dom, (dom,ci), (dom,ci))]),ctxm(beta_2_r_,r,sr, (i,s,beta_2_), (c,s,beta_2_))]),ctxm(beta_2_r_,r,dom, (dom,r,beta_2_), (dom,r,beta_2_))]),ctxm(beta_2_r_,r,ip, (ip,r), (ip,r)),ctxm(beta_2_r_,u,d_2, (i,d_2), (c,d_2)),ctxm(beta_2_r_,u,d_5, (i,d_5), (c,d_5))]))).